$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it f2f+}$:F2F+{-}decls, ${\it sndr}$, ${\it rcvr}$:${\it ff}$.C, $e$, ${\it e'}$:E.
\\[0ex]plus{-}ify\{i:l\}(${\it es}$;${\it ff}$;is\_req  ;is\_ack ;awaiting ;owes\_ack )
\\[0ex]$\Rightarrow$ (f2f+{-}pred($e$,${\it e'}$) $\Leftarrow\!\Rightarrow$ (f2f+{-}p+!($e$,${\it e'}$)))